\begin{tabbing}
$\forall$$R$:Realizer.
\\[0ex]R{-}Feasible($R$)
\\[0ex]$\Rightarrow$ \=($\forall$$f$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$).\+
\\[0ex]($\forall$$i$, $x$:Id. ($\uparrow<$$i$, $x$$>$ $\in$ dom(R{-}discrete($R$))) $\Rightarrow$ (R{-}discrete($R$)($<$$i$, $x$$>$) = $f$($i$,$x$)))
\\[0ex]$\Rightarrow$ d{-}feasible{-}discrete([[$R$]];$f$))
\-
\end{tabbing}